;;;===========================================================================
;;;
;;; Supension construction
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 24/05/10 || End date: 24/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "algebraic-data-structures")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring *) => *)
 ;; Addition operation ring
 ((addition-ring * *)=> *)
 ;; Product operation ring
 ((product-ring * *) => *)
 ;; Inverse ring
 ((inverse *) => *)
 ;; Zero element ring
 ((zero-element ) => *)
 ;; Unit element ring
 ((unit )=> *)


 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C * *) => *)
 ;; Group Operation 
 ((group-operation-C * * *) => *)
 ;; Zero element
 ((zero-C *) => *)
 ;; External multiplication
 ((external-C * * *) => *)
 ;; Inverse element
 ((inverse-C * *) => *)

 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------

 ;; The differential
 ((d-C * *) => *)
 
 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element nil
	  0))

 ;; Unit element ring
 (local (defun unit nil
	  1))



 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse C
 (local (defun inverse-C (n a)
	  (declare (ignore n a))
	  0))

 


 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------
 
  ;; The differential
 (local (defun d-C (n a)
	  (declare (ignore n a))
	  0))


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 
  

 (check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-c :group-operation-cc 'group-operation-c :zero-cc 'zero-c :external-cc 'external-c
		    :inverse-cc 'inverse-c :d-cc 'd-c)
 'C)




)


;;==================================================
;; The Suspension definitions
;;==================================================


 ;;--------------------------------------------------
 ;; Suspension Chain Complex 
 ;;--------------------------------------------------

 ;; Characteristic function
(defun inv-suspension (n a) 
  (inv-C (1- n) a)
  )

 ;; Group Operation 
(defun group-operation-suspension (n a b)
   (group-operation-C (1- n) a b)
   )
	  

 ;; Zero element
(defun zero-suspension (n)
   (zero-C (1- n))
   )
   

 ;; External multiplication
(defun external-suspension (n a b)
   (external-c (1- n) a b)
   	 )

 ;; Inverse element
(defun inverse-suspension (n a)
   (inverse-C (1- n) a)
   )
	 

 ;;--------------------------------------------------
 ;; Suspension differential 
 ;;--------------------------------------------------

 ;; The differential
(defun d-suspension (n a)
  (inverse-C (1- (1- n)) (d-c (1- n) a)
	  ))


 ;;--------------------------------------------------
 ;; The Suspension is a Chain Complex 
 ;;--------------------------------------------------

(defthm group-operation-C-distrivutivity
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(integerp n))
	   (equal (group-operation-c n a (group-operation-c n b c))
		  (group-operation-c n c (group-operation-c n a b))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |C-is-a-chain-complex|)))))


(defthm group-operation-C-distrivutivity-bis
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(integerp n))
	   (equal (group-operation-c n a (group-operation-c n b c))
		  (group-operation-c n b (group-operation-c n a c))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-C-distrivutivity)))))


(in-theory (disable COMMUTATIVITY-OF-+
		    ASSOCIATIVITY-OF-+))


(defthm inv-inverse-d
  (implies (and (inv-c (+ n -1) a)
		(integerp n))
	   (INV-C (+ (+ N -1) -1)
                (INVERSE-C (+ (+ N -1) -1)
                           (D-C (+ N -1) A)))))


(defthm inverse-operation=operation-inverse
  (IMPLIES (AND (INV-C (+ n -1)  A)
              (INV-C (+ n -1) B)
              (INTEGERP N))
         (EQUAL (INVERSE-C (+ (+ N -1) -1)
                           (GROUP-OPERATION-C (+ (+ N -1) -1)
                                              (D-C (+ n -1) A)
                                              (D-C (+ n -1) B)))
                (GROUP-OPERATION-C (+ (+ N -1) -1)
                                   (INVERSE-C (+ (+ N -1) -1) (D-C (+ n -1) A))
                                   (INVERSE-C (+ (+ N -1) -1)
                                              (D-C (+ n -1) B)))))
)


(defthm inverse-external
  (IMPLIES (AND (INV-C (+ N -1) A)
              (INV-RING R)
              (INTEGERP N))
         (EQUAL (INVERSE-C (+ (+ N -1) -1)
                           (EXTERNAL-C (+ (+ N -1) -1)
                                       R (D-C (+ N -1) A)))
                (EXTERNAL-C (+ (+ N -1) -1)
                            R
                            (INVERSE-C (+ (+ N -1) -1)
                                       (D-C (+ N -1) A))))))

(defthm d-d-zero-help
  (IMPLIES
     (AND (INV-C (+ (+ (+ N -1) -1) -1)  A) (INTEGERP N))
     (EQUAL (INVERSE-C (+ (+ (+ N -1) -1) -1)
                       (INVERSE-C (+ (+ (+ N -1) -1) -1)
                                  a))
            a)))


(defthm d-d-zero-help-2
  (IMPLIES (AND (INV-C (+ N -1) A) (INTEGERP N))
         (EQUAL (D-C (+ (+ N -1) -1) (D-C (+ N -1) A))
                (ZERO-C (+ (+ (+ N -1) -1) -1))))
  :hints (("Goal" :in-theory (enable COMMUTATIVITY-OF-+))))



(defthm d-d-zero
  (IMPLIES (AND (INV-C (+ N -1) A) (INTEGERP N))
         (EQUAL (INVERSE-C (+ (+ (+ N -1) -1) -1)
                           (D-C (+ (+ N -1) -1)
                                (INVERSE-C (+ (+ N -1) -1)
                                           (D-C (+ N -1) A))))
                (ZERO-C (+ (+ (+ N -1) -1) -1)))))

(in-theory (enable COMMUTATIVITY-OF-+))

(defthm inv-inverse-d-bis
  (IMPLIES (AND (INV-C (+ -1 N) A) (INTEGERP N))
         (INV-C (+ -1 -1 N)
                (INVERSE-C (+ -1 -1 N)
                           (D-C (+ -1 N) A))))
  :hints (("Goal" :use (:instance inv-inverse-d))))

(defthm inverse-operation=operation-inverse-bis
  (IMPLIES (AND (INV-C (+ -1 N) A)
              (INV-C (+ -1 N) B)
              (INTEGERP N))
         (EQUAL (INVERSE-C (+ -1 -1 N)
                           (GROUP-OPERATION-C (+ -1 -1 N)
                                              (D-C (+ -1 N) A)
                                              (D-C (+ -1 N) B)))
                (GROUP-OPERATION-C (+ -1 -1 N)
                                   (INVERSE-C (+ -1 -1 N) (D-C (+ -1 N) A))
                                   (INVERSE-C (+ -1 -1 N)
                                              (D-C (+ -1 N) B)))))
:hints (("Goal" :use (:instance inverse-operation=operation-inverse))))


(defthm inverse-external-bis
  (IMPLIES (AND (INV-C (+ -1 N) A)
              (INV-RING R)
              (INTEGERP N))
         (EQUAL (INVERSE-C (+ -1 -1 N)
                           (EXTERNAL-C (+ -1 -1 N)
                                       R (D-C (+ -1 N) A)))
                (EXTERNAL-C (+ -1 -1 N)
                            R
                            (INVERSE-C (+ -1 -1 N)
                                       (D-C (+ -1 N) A)))))
  :hints (("Goal" :use (:instance inverse-external))))


(defthm d-d-zero-bis
  (IMPLIES (AND (INV-C (+ -1 N) A) (INTEGERP N))
         (EQUAL (INVERSE-C (+ -1 -1 -1 N)
                           (D-C (+ -1 -1 N)
                                (INVERSE-C (+ -1 -1 N)
                                           (D-C (+ -1 N) A))))
                (ZERO-C (+ -1 -1 -1 N))))
 :hints (("Goal" :use (:instance d-d-zero))))



(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-suspension :group-operation-cc 'group-operation-suspension :zero-cc 'zero-suspension :external-cc 'external-suspension
		    :inverse-cc 'inverse-suspension :d-cc 'd-suspension)
 'suspension-C)


;;;===========================================================================
;;;
;;; End of the suspension construction
;;;
;;;===========================================================================



;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(inv-suspension
   group-operation-suspension
   zero-suspension
   external-suspension
   inverse-suspension
   d-suspension
   |SUSPENSION-C-is-a-chain-complex|
   )
 )
|#


(defconst *suspension*
  '((DEFUN INV-SUSPENSION (N A)
        (INV-C (1- N) A))
 (DEFUN GROUP-OPERATION-SUSPENSION (N A B)
        (GROUP-OPERATION-C (1- N) A B))
 (DEFUN ZERO-SUSPENSION (N)
        (ZERO-C (1- N)))
 (DEFUN EXTERNAL-SUSPENSION (N A B)
        (EXTERNAL-C (1- N) A B))
 (DEFUN INVERSE-SUSPENSION (N A)
        (INVERSE-C (1- N) A))
 (DEFUN D-SUSPENSION (N A)
        (INVERSE-C (1- (1- N)) (D-C (1- N) A)))
 (DEFTHM
  |SUSPENSION-C-is-a-chain-complex|
  (AND
   (AND
    (AND
      (AND (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
      (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                         (INV-RING (PRODUCT-RING X Y)))
                (IMPLIES (AND (INV-RING X)
                              (INV-RING Y)
                              (INV-RING Z))
                         (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                (PRODUCT-RING X (PRODUCT-RING Y Z)))))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING (UNIT) X) X))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING X (UNIT)) X))
           (INV-RING (UNIT)))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                      (ADDITION-RING (PRODUCT-RING X Y)
                                     (PRODUCT-RING X Z))))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                      (ADDITION-RING (PRODUCT-RING X Z)
                                     (PRODUCT-RING Y Z)))))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-SUSPENSION N B)
                  (INTEGERP N))
             (INV-SUSPENSION N (GROUP-OPERATION-SUSPENSION N A B)))
    (IMPLIES
     (AND (INV-SUSPENSION N A)
          (INV-SUSPENSION N B)
          (INV-SUSPENSION N C)
          (INTEGERP N))
     (EQUAL
          (GROUP-OPERATION-SUSPENSION N (GROUP-OPERATION-SUSPENSION N A B)
                                      C)
          (GROUP-OPERATION-SUSPENSION N
                                      A (GROUP-OPERATION-SUSPENSION N B C))))
    (INV-SUSPENSION N (ZERO-SUSPENSION N))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-RING R)
                  (INTEGERP N))
             (INV-SUSPENSION N (EXTERNAL-SUSPENSION N R A)))
    (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-SUSPENSION N A (ZERO-SUSPENSION N))
                    A))
    (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
             (INV-SUSPENSION N (INVERSE-SUSPENSION N A)))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-SUSPENSION N B)
                  (INTEGERP N)
                  (EQUAL (GROUP-OPERATION-SUSPENSION N A B)
                         (ZERO-SUSPENSION N)))
             (EQUAL (INVERSE-SUSPENSION N A) B))
    (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-SUSPENSION N A (INVERSE-SUSPENSION N A))
                    (ZERO-SUSPENSION N)))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-SUSPENSION N B)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-SUSPENSION N A B)
                    (GROUP-OPERATION-SUSPENSION N B A)))
    (IMPLIES
         (AND (INV-SUSPENSION N A)
              (INV-SUSPENSION N B)
              (INV-RING R)
              (INTEGERP N))
         (EQUAL (EXTERNAL-SUSPENSION N R (GROUP-OPERATION-SUSPENSION N A B))
                (GROUP-OPERATION-SUSPENSION N (EXTERNAL-SUSPENSION N R A)
                                            (EXTERNAL-SUSPENSION N R B))))
    (IMPLIES
         (AND (INV-SUSPENSION N A)
              (INV-RING S)
              (INV-RING R)
              (INTEGERP N))
         (EQUAL (EXTERNAL-SUSPENSION N (ADDITION-RING S R)
                                     A)
                (GROUP-OPERATION-SUSPENSION N (EXTERNAL-SUSPENSION N S A)
                                            (EXTERNAL-SUSPENSION N R A))))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-RING S)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-SUSPENSION N (PRODUCT-RING S R)
                                         A)
                    (EXTERNAL-SUSPENSION N S (EXTERNAL-SUSPENSION N R A))))
    (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
             (EQUAL (EXTERNAL-SUSPENSION N (UNIT) A)
                    A))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-SUSPENSION N B)
                  (INTEGERP N))
             (EQUAL (INVERSE-SUSPENSION N (GROUP-OPERATION-SUSPENSION N A B))
                    (GROUP-OPERATION-SUSPENSION N (INVERSE-SUSPENSION N A)
                                                (INVERSE-SUSPENSION N B))))
    (IMPLIES (AND (INV-SUSPENSION N A)
                  (INV-RING S)
                  (INTEGERP N))
             (EQUAL (INVERSE-SUSPENSION N (EXTERNAL-SUSPENSION N S A))
                    (EXTERNAL-SUSPENSION N S (INVERSE-SUSPENSION N A))))
    (IMPLIES (INTEGERP N)
             (EQUAL (INVERSE-SUSPENSION N (ZERO-SUSPENSION N))
                    (ZERO-SUSPENSION N)))
    (IMPLIES (AND (INV-RING S) (INTEGERP N))
             (EQUAL (EXTERNAL-SUSPENSION N S (ZERO-SUSPENSION N))
                    (ZERO-SUSPENSION N))))
   (AND
     (AND (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
                   (INV-SUSPENSION (+ N -1)
                                   (D-SUSPENSION N A)))
          (IMPLIES (AND (INV-SUSPENSION N A)
                        (INV-SUSPENSION N B)
                        (INTEGERP N))
                   (EQUAL (D-SUSPENSION N (GROUP-OPERATION-SUSPENSION N A B))
                          (GROUP-OPERATION-SUSPENSION (+ N -1)
                                                      (D-SUSPENSION N A)
                                                      (D-SUSPENSION N B))))
          (IMPLIES (AND (INV-SUSPENSION N A)
                        (INV-RING R)
                        (INTEGERP N))
                   (EQUAL (D-SUSPENSION N (EXTERNAL-SUSPENSION N R A))
                          (EXTERNAL-SUSPENSION (+ N -1)
                                               R (D-SUSPENSION N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (D-SUSPENSION N (ZERO-SUSPENSION N))
                          (ZERO-SUSPENSION (+ N -1))))
          (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
                   (EQUAL (D-SUSPENSION N (INVERSE-SUSPENSION N A))
                          (INVERSE-SUSPENSION (+ N -1)
                                              (D-SUSPENSION N A)))))
     (IMPLIES (AND (INV-SUSPENSION N A) (INTEGERP N))
              (EQUAL (D-SUSPENSION (1- N) (D-SUSPENSION N A))
                     (ZERO-SUSPENSION (1- (1- N)))))))))
)


(make-generic-theory *suspension*)